A:msga{i:l}, dec:(b:IdA.state(TopA.da(locl(b))Top+Top)), a:Atom1.
atom-free-decl{i:l}
atom-free-decl(Id; IdDeq; ds(A))
 atom-free-decl{i:l}
 atom-free-decl(Knd; KindDeq; da(A))
 local-atom{i:l}(A; dec; a)  Prop{i'} 

latex

Definitions

t  T, P  Q, x:A. B(x), MsgA, Top, locl(a), M.da(a), x:AB(x), left+right, M.state, x:AB(x), Id, Atom$n, ds(M), IdDeq, AtomFree(d), da(M), KindDeq, Knd, f(a), x.A(x), nat-deq-aux, <a,b>, NatDeq, atom-deq-aux, AtomDeq, #$n, a<b, Void, False, A, AB, , {x:A| B(x) }, , Atom, prod-deq(A;B;a;b), proddeq(a;b), product-deq(A;B;a;b), IdLnkDeq, IdLnk, sum-deq(A;B;a;b), sumdeq(a;b), union-deq(A;B;a;b), Type, AtomFree(T;x), x:T>>a, True, Prop, P  Q, ma-body(M), Shape(M), local-atom(A;dec;a)

Lemmas

ma-shape wf, ma-body wf, true wf, inheres wf, Knd wf, Kind-deq wf, ma da wf, atom-free-decl wf, id-deq wf, ma ds wf, Id wf, ma-st wf, ma-da wf, locl wf, top wf, msga wf, atom-free-ma-shape, atom-free-ma-decider